es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
f2f+-pred(e',e)  ([e: sndr is_req   rcvr]  [e: rcvr is_ack  sndr]) 

latex

Definitions	t  T, P  Q, x:A. B(x), P & Q, {T},
Lemmas	event system wf, FIFO wf, F2F+-decls wf, fifoC wf, es-E wf, f2f+-pred wf, f2f+-pred-field